Step of Proof: nat_ind_tp 9,38
Inference at * 1 1 1 2 1 1 
Iof proof for Lemma nat ind tp:

.....basecase..... NILNIL

1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
  P(0) 
latex
 by %E% Hypothesis 
latex

 .

origin